FDL - Nuprl Lemma : conditional_wf2

Nuprl Lemma : conditional_wf2

T, V:Type, A, B:(T

), dcd_A:(t:T

Dec(A(t))), f:({t:T| A(t)}

V), g:({t:T| B(t)}

V).
[

t.A(t)? f : g]

{t:T| A(t)

B(t)}

V

Definitions f(a), x(s), {x:A| B(x)} , x:AB(x), left + right, P Q, A, t T, Void, P Q, False, x:A. B(x), S T, suptype(S; T), Type, , Dec(P), x.A(x), [P? f : g], <a, b>, s = t, x. t(x)

Lemmas not wf, subtype rel function, subtype rel set, conditional wf, decidable wf